r:Rng. (1 = 0  |r|)  (a:|r|. a = 0) 

latex

Up	rings 1
Definitions of Statement	Rng
Definitions	, t  T, P  Q, x:A. B(x), P  Q, P & Q, P  Q, x f y, Rng
Lemmas	rng wf, rng zero wf, rng one wf, rng car wf, rng times one, rng times zero, rng times wf